%include
:- lib(ic).

coffeemachineCoffeemachine(Args , Result , NState):-

NState = [Money], 
Args = [],
Result = [],
 
% domains of variables
[Money]:: -32768 ..32767,
 
% invariants before call
MoneyPre #>= 0,
MoneyPre #=< 100,

% preconditions

% postconditions
Money #= 0,
 
% invariants after call
Money #>= 0,
Money #=< 100,
 
% solving constraints
indomain(Money).
 
coffeemachineInsert(OState , Args , Result , NState):-

% variables
OState = [MoneyPre], 
NState = [Money], 
Args = [C], 
Result = [],
 
% domains of variables
[Money]:: -32768 ..32767,
 
% invariants before call
MoneyPre #>= 0,
MoneyPre #=< 100,

% preconditions
C #> 0,
C #=< 10,

% postconditions
Money #= MoneyPre + C * 10,
 
% invariants after call
Money #>= 0,
Money #=< 100,
 
% solving constraints
indomain(Money).
 
coffeemachineWithdraw(OState , Args , Result , NState):-

% variables
OState = [MoneyPre], 
NState = [Money], 
Args = [],
 
% domains of variables
[Money]:: -32768 ..32767,
 
% invariants before call
MoneyPre #>= 0,
MoneyPre #=< 100,

% preconditions

% postconditions
Result #= MoneyPre,
Money #= 0,
 
% invariants after call
Money #>= 0,
Money #=< 100,
 
% solving constraints
indomain(Money).
 
coffeemachineCook(OState , Args , Result , NState):-

% variables
OState = [MoneyPre], 
NState = [Money], 
Args = [],
Result = [],
 
% domains of variables
[Money]:: -32768 ..32767,
 
% invariants before call
MoneyPre #>= 0,
MoneyPre #=< 100,

% preconditions

% postconditions
Money #= MoneyPre - 10,
 
% invariants after call
Money #>= 0,
Money #=< 100,
 
% solving constraints
indomain(Money).
 
coffeemachineDone(OState , Args , Result , NState):-

% variables
OState = [MoneyPre], 
NState = [Money], 
Args = [],
 
% domains of variables
[Money]:: -32768 ..32767,
 
% invariants before call
MoneyPre #>= 0,
MoneyPre #=< 100,

% preconditions

% postconditions
Result = ["Coffee is ready. Thank you!"],
Money #= MoneyPre,
 
% invariants after call
Money #>= 0,
Money #=< 100,
 
% solving constraints
indomain(Money).
 

coffeemachineDoneGuard1(OState , Args , Result , NState):-
% variables
OState = [MoneyPre], 
NState = [Money], 
Args = [],
Result = [],
 
% guard conditions
MoneyPre #>=  10,
 
% state update
Money #= MoneyPre.

coffeemachineDoneGuard2(OState , Args , Result , NState):-
% variables
OState = [MoneyPre], 
NState = [Money], 
Args = [],
Result = [],
 
% guard conditions
MoneyPre #= 0,
 
% state update
Money #= MoneyPre.
 
%path 
testpath(Args , Results , NState):-
 
coffeemachineCoffeemachine(Arg0 , Res0 , S0),
NState = [S0|NState1],
Args = [Arg0|A0],
Results = [Res0|R0],
 
coffeemachineInsert(S0 , Arg1 , Res1 , S1),
NState1= [S1|NState2],
A0= [Arg1|A1],
R0= [Res1|R1],
 
coffeemachineWithdraw(S1 , Arg2 , Res2 , S2),
NState2= [S2|NState3],
A1= [Arg2|A2],
R1= [Res2|R2],
 
coffeemachineInsert(S2 , Arg3 , Res3 , S3),
NState3= [S3|NState4],
A2= [Arg3|A3],
R2= [Res3|R3],
 
coffeemachineCook(S3 , Arg4 , Res4 , S4),
NState4= [S4|NState5],
A3= [Arg4|A4],
R3= [Res4|R4],
 
coffeemachineWithdraw(S4 , Arg5 , Res5 , S5),
NState5= [S5|NState6],
A4= [Arg5|A5],
R4= [Res5|R5],
 
coffeemachineDoneGuard1(S5 , Arg6 , Res6 , S6),
NState6= [S6|NState7],
A5= [Arg6|A6],
R5= [Res6|R6],
 
coffeemachineDone(S6 , Arg7 , Res7 , S7),
NState7= [S7|NState8],
A6= [Arg7|A7],
R6= [Res7|R7],
 
coffeemachineInsert(S7 , Arg8 , Res8 , S8),
NState8= [S8|NState9],
A7= [Arg8|A8],
R7= [Res8|R8],
 
coffeemachineWithdraw(S8 , Arg9 , Res9 , S9),
NState9= [S9],
A8= [Arg9],
R8= [Res9].
